Nuprl Lemma : fincr_wf
2,24
postcript
pdf
FIncr
Type
latex
Definitions
FIncr
,
t
T
,
if
b
t
else
f
fi
,
{
i
...}
,
,
x
:
A
.
B
(
x
)
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
x
(
s
)
,
{
T
}
,
T
,
True
,
P
Q
,
Prop
,
A
B
,
A
,
False
,
i
j
,
x
f
y
,
i
=
j
,
P
Q
,
a
b
Lemmas
int
upper
wf
,
eq
int
eq
false
elim
sqequal
,
eq
int
eq
true
elim
sqequal
,
bool
cases
sqequal
,
eq
int
wf
,
nat
properties
,
ge
wf
,
le
wf
,
nat
wf
origin
T, if b
t else f fi, {i...}, 
, 
x:A. B(x), WellFnd{i}(A;x,y.R(x;y)), x(s), {T}, 
T, True, P 
Q, Prop, A
B, 
A, False, i
j, x f y, i=
j, P 
Q, a 
b